IrrelevantIndexNotInconsistent.agda:23,15-16
b != b₁ of type Bool
when checking that the expression p has type True b₁
